Search results for "Homotopy lifting property"
showing 4 items of 4 documents
Homotopy limits for 2-categories
2008
AbstractWe study homotopy limits for 2-categories using the theory of Quillen model categories. In order to do so, we establish the existence of projective and injective model structures on diagram 2-categories. Using these results, we describe the homotopical behaviour not only of conical limits but also of weighted limits. Finally, pseudo-limits are related to homotopy limits.
On the proper homotopy invariance of the Tucker property
2006
A non-compact polyhedron P is Tucker if, for any compact subset K ⊂ P, the fundamental group π1(P − K) is finitely generated. The main result of this note is that a manifold which is proper homotopy equivalent to a Tucker polyhedron is Tucker. We use Poenaru’s theory of the equivalence relations forced by the singularities of a non-degenerate simplicial map.
Discrete and differential homotopy in circular restricted three-body control
2010
The planar circular restricted three-body problem is considered. The control enters linearly in the equation of motion to model the thrust of the third body. The minimum time optimal control problem has two scalar parameters: The ratio of the primaries masses which embeds the two-body problem into the three-body one, and the upper bound on the control norm. Regular extremals of the maximum principle are computed by shooting thanks to continuations with respect to both parameters. Discrete and dierential homotopy are compared in connection with second order sucient conditions in optimal control. Homotopy with respect to control bound gives evidence of various topological structures of extr…
Inductive types in homotopy type theory
2012
Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof s…